0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 16 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 0 ms)
↳10 QDP
↳11 MRRProof (⇔, 7 ms)
↳12 QDP
↳13 PisEmptyProof (⇔, 0 ms)
↳14 YES
average_in_gga(0, 0, 0) → average_out_gga(0, 0, 0)
average_in_gga(0, s(0), 0) → average_out_gga(0, s(0), 0)
average_in_gga(0, s(s(0)), s(0)) → average_out_gga(0, s(s(0)), s(0))
average_in_gga(s(X), Y, Z) → U1_gga(X, Y, Z, average_in_gga(X, s(Y), Z))
average_in_gga(X, s(s(s(Y))), s(Z)) → U2_gga(X, Y, Z, average_in_gga(s(X), Y, Z))
U2_gga(X, Y, Z, average_out_gga(s(X), Y, Z)) → average_out_gga(X, s(s(s(Y))), s(Z))
U1_gga(X, Y, Z, average_out_gga(X, s(Y), Z)) → average_out_gga(s(X), Y, Z)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
average_in_gga(0, 0, 0) → average_out_gga(0, 0, 0)
average_in_gga(0, s(0), 0) → average_out_gga(0, s(0), 0)
average_in_gga(0, s(s(0)), s(0)) → average_out_gga(0, s(s(0)), s(0))
average_in_gga(s(X), Y, Z) → U1_gga(X, Y, Z, average_in_gga(X, s(Y), Z))
average_in_gga(X, s(s(s(Y))), s(Z)) → U2_gga(X, Y, Z, average_in_gga(s(X), Y, Z))
U2_gga(X, Y, Z, average_out_gga(s(X), Y, Z)) → average_out_gga(X, s(s(s(Y))), s(Z))
U1_gga(X, Y, Z, average_out_gga(X, s(Y), Z)) → average_out_gga(s(X), Y, Z)
AVERAGE_IN_GGA(s(X), Y, Z) → U1_GGA(X, Y, Z, average_in_gga(X, s(Y), Z))
AVERAGE_IN_GGA(s(X), Y, Z) → AVERAGE_IN_GGA(X, s(Y), Z)
AVERAGE_IN_GGA(X, s(s(s(Y))), s(Z)) → U2_GGA(X, Y, Z, average_in_gga(s(X), Y, Z))
AVERAGE_IN_GGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GGA(s(X), Y, Z)
average_in_gga(0, 0, 0) → average_out_gga(0, 0, 0)
average_in_gga(0, s(0), 0) → average_out_gga(0, s(0), 0)
average_in_gga(0, s(s(0)), s(0)) → average_out_gga(0, s(s(0)), s(0))
average_in_gga(s(X), Y, Z) → U1_gga(X, Y, Z, average_in_gga(X, s(Y), Z))
average_in_gga(X, s(s(s(Y))), s(Z)) → U2_gga(X, Y, Z, average_in_gga(s(X), Y, Z))
U2_gga(X, Y, Z, average_out_gga(s(X), Y, Z)) → average_out_gga(X, s(s(s(Y))), s(Z))
U1_gga(X, Y, Z, average_out_gga(X, s(Y), Z)) → average_out_gga(s(X), Y, Z)
AVERAGE_IN_GGA(s(X), Y, Z) → U1_GGA(X, Y, Z, average_in_gga(X, s(Y), Z))
AVERAGE_IN_GGA(s(X), Y, Z) → AVERAGE_IN_GGA(X, s(Y), Z)
AVERAGE_IN_GGA(X, s(s(s(Y))), s(Z)) → U2_GGA(X, Y, Z, average_in_gga(s(X), Y, Z))
AVERAGE_IN_GGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GGA(s(X), Y, Z)
average_in_gga(0, 0, 0) → average_out_gga(0, 0, 0)
average_in_gga(0, s(0), 0) → average_out_gga(0, s(0), 0)
average_in_gga(0, s(s(0)), s(0)) → average_out_gga(0, s(s(0)), s(0))
average_in_gga(s(X), Y, Z) → U1_gga(X, Y, Z, average_in_gga(X, s(Y), Z))
average_in_gga(X, s(s(s(Y))), s(Z)) → U2_gga(X, Y, Z, average_in_gga(s(X), Y, Z))
U2_gga(X, Y, Z, average_out_gga(s(X), Y, Z)) → average_out_gga(X, s(s(s(Y))), s(Z))
U1_gga(X, Y, Z, average_out_gga(X, s(Y), Z)) → average_out_gga(s(X), Y, Z)
AVERAGE_IN_GGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GGA(s(X), Y, Z)
AVERAGE_IN_GGA(s(X), Y, Z) → AVERAGE_IN_GGA(X, s(Y), Z)
average_in_gga(0, 0, 0) → average_out_gga(0, 0, 0)
average_in_gga(0, s(0), 0) → average_out_gga(0, s(0), 0)
average_in_gga(0, s(s(0)), s(0)) → average_out_gga(0, s(s(0)), s(0))
average_in_gga(s(X), Y, Z) → U1_gga(X, Y, Z, average_in_gga(X, s(Y), Z))
average_in_gga(X, s(s(s(Y))), s(Z)) → U2_gga(X, Y, Z, average_in_gga(s(X), Y, Z))
U2_gga(X, Y, Z, average_out_gga(s(X), Y, Z)) → average_out_gga(X, s(s(s(Y))), s(Z))
U1_gga(X, Y, Z, average_out_gga(X, s(Y), Z)) → average_out_gga(s(X), Y, Z)
AVERAGE_IN_GGA(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GGA(s(X), Y, Z)
AVERAGE_IN_GGA(s(X), Y, Z) → AVERAGE_IN_GGA(X, s(Y), Z)
AVERAGE_IN_GGA(X, s(s(s(Y)))) → AVERAGE_IN_GGA(s(X), Y)
AVERAGE_IN_GGA(s(X), Y) → AVERAGE_IN_GGA(X, s(Y))
AVERAGE_IN_GGA(X, s(s(s(Y)))) → AVERAGE_IN_GGA(s(X), Y)
AVERAGE_IN_GGA(s(X), Y) → AVERAGE_IN_GGA(X, s(Y))
s1 > AVERAGEINGGA2
s_1=1
AVERAGE_IN_GGA_2=0